1. Technical Field
This disclosure generally relates to constraint solvers. More specifically, this disclosure relates to methods and apparatuses for identifying a set of inconsistent constraints.
2. Related Art
The importance of circuit verification cannot be over-emphasized. Indeed, without circuit verification it would have been impossible to design complicated integrated circuits which are commonly found in today's computing devices.
Constrained random simulation methodologies have become increasingly popular for functional verification of complex designs, as an alternative to directed-test based simulation. In a constrained random simulation methodology, random vectors are generated to satisfy certain operating constraints of the design. These constraints are usually specified as part of a test-bench program. A test-bench automation tool (TBA) uses the test-bench program to generate random solutions for a set of random variables, such that a set of constraints over the set of random variables is satisfied. These random solutions can then be used to generate valid random stimulus for the Design Under Verification (DUV). This stimulus is simulated using simulation tools, and the results of the simulation are typically examined within the test-bench program to monitor functional coverage, thereby providing a measure of confidence on the verification quality and completeness.
Constraint solvers are typically used to generate random vectors that satisfy the set of constraints. Constraint solvers solve the following constraint satisfaction problem: given a set of random variables and a set of constraints, assign a set of random values to the set of random variables that satisfy the set of constraints. Note that, if the set of constraints are inconsistent, the constraint solver will not be able to assign random values to the random variables that satisfy the set of constraints. Therefore, it is generally desirable to be able to identify inconsistencies in a set of constraints.